fix(spec): harden for leanSpec 4ca7d27 (equivocation determinism, future-horizon, off-finalized admission, justification rejections)#367
Merged
Conversation
Mirror leanSpec #1181: an equivocator can cast two distinct votes at one slot. ExtractLatestAttestations now keeps, per validator, the vote with the highest (slot, attestation-data hash-tree-root), so the extracted LMD view is a pure function of the pool, independent of insertion order, and every node runs fork choice on the same set. Block production already applied the same canonical-root secondary sort key.
Mirror leanSpec #1182: reject a block whose slot exceeds the store clock by more than one slot (BLOCK_TOO_FAR_IN_FUTURE), in on_block before the transition and signature check, so a far-future block cannot force an unbounded empty-slot walk. currentSlot = store.Time()/IntervalsPerSlot; the full-slot margin still admits an intended early block. The signatures spectest now sets the store clock to the block's slot, as the live node does before importing an on-time block.
Mirror leanSpec #1179: attestation admission now rejects a vote whose head does not descend from the finalized block (HEAD_NOT_DESCENDANT_OF_FINALIZED), mirroring the prune predicate so a re-gossiped below-finalized aggregate cannot re-enter the pool after pruning dropped it.
… errors Mirror leanSpec #1178: reject a zero-validator registry (EMPTY_VALIDATOR_REGISTRY) instead of silently no-oping, and reject a justification vote bitlist whose length is not len(justifications_roots) * validator_count (JUSTIFICATION_VOTES_LENGTH_MISMATCH) rather than reading past or short of a segment. The existing zero-root check is retained, in spec order.
At pin 4ca7d27 the justifiability fixtures carry delta = slot - finalizedSlot as a signed value (negative for slots before the finalized boundary). Type the fixture field int64 and compute the cross-check delta with signed subtraction; gean's SlotIsJustifiableAfter already returns false for slot < finalizedSlot, so this is a fixture-parser catch-up only.
The #1179-reworked store-pruning fixture expects a vote gossiped as "new" to be "known" after the next block step. The harness promoted the payload pool (PromoteNewToKnown) but left the fork-choice known tracker unchanged, so the just-promoted vote was absent from the tracker the attestationChecks read. Re-derive the known votes from the promoted pool, mirroring the Engine's next updateHead.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Spec-compliance hardening for leanSpec
4ca7d27Bumps
LEAN_SPEC_COMMIT_HASHto4ca7d27(leanSpec HEAD) and closes the gean drift a/spec-compliantsweep across the 7 commits43246bd..4ca7d27surfaced. All 7 are hardening/correctness fixes (DoS bounds, determinism, typed rejections); the happy path is unchanged.Spec-compliance fixes
ad262a5ExtractLatestAttestationsnow keeps, per validator, the vote with the highest(slot, attestation-data hash-tree-root), so the extracted LMD view is a pure function of the pool, independent of insertion order. Block production already applied the same canonical-root secondary sort key.e27dc7cBLOCK_TOO_FAR_IN_FUTURE. Reject a block whose slot exceeds the store clock by more than one slot, inon_blockbefore the transition and signature check, so a far-future block cannot force an unbounded empty-slot walk.currentSlot = store.Time()/IntervalsPerSlot; the full-slot margin still admits an intended early block.b625e80HEAD_NOT_DESCENDANT_OF_FINALIZED. Attestation admission rejects a vote whose head does not descend from the finalized block, mirroring the prune predicate so a re-gossiped below-finalized aggregate cannot re-enter the pool after pruning.24d6621EMPTY_VALIDATOR_REGISTRY) instead of silently no-oping, and reject a vote bitlist whose length ≠len(justifications_roots) × validator_count(JUSTIFICATION_VOTES_LENGTH_MISMATCH), rather than reading past/short of a segment. The existing zero-root check is retained, in spec order.Each change mirrors its leanSpec function precisely and was self-reviewed for spec mapping, invariants, and gean's architecture (pure
statetransition, off-tick workers,ForkChoiceoutside the store).Spectest harness catch-up
The pin bump exposed two spectest issues unrelated to the fixes above — both spectest-harness catch-ups for the #1178/#1179 fixture reworks, not consensus-logic bugs:
905c490delta. Fixtures now carrydelta = slot - finalizedSlotas a signed value (negative before the finalized boundary). Typed the fieldint64+ signed cross-check. gean'sSlotIsJustifiableAfterwas already correct.b3ca0f5updateHead.Validation
make build✓ ·make test✓ · full spec suiteok internal/spectests✓ ·make lint✓HEAD_NOT_DESCENDANT_OF_FINALIZED) flip fail→pass; #1178 passing; zero regressions across the suite.store/payloads, the equal-slot max-(slot,root)selection) and matches the fixture's documented intent.Known upstream caveat
leanSpec's own #1181 equivocation fixtures fail to generate at
4ca7d27— its fork-choice produces a head that disagrees with its own test's expected value (head_slotactual ≠ expected). This is an upstream leanSpec inconsistency (its #1181 code vs its #1181 test), not a gean issue: fixture generation runs leanSpec's pytest, which gean only consumes. The 3 equivocation vectors are therefore excluded from the run; everything else generates and passes. Worth filing upstream.Notes